a,b:Knd. decidable((a = b)) 

latex

Definitions	x:A. B(x), P  Q, P  Q, prop{i:l}, t  T, x. t(x), P  Q, P  Q, x(s)
Lemmas	all functionality wrt iff, Knd wf, decidable wf, assert wf, eq knd wf, decidable functionality, assert-eq-knd, decidable assert